package simple;
import JaCoP.constraints.AndBool;
import JaCoP.constraints.OrBool;
import JaCoP.constraints.XorBool;
import JaCoP.core.IntVar;
import JaCoP.core.Store;
import JaCoP.search.DepthFirstSearch;
import JaCoP.search.IndomainMin;
import JaCoP.search.PrintOutListener;
import JaCoP.search.Search;
import JaCoP.search.SelectChoicePoint;
import JaCoP.search.SimpleSelect;

public class FullAdder1 {

	/**
	 * @param args
	 */
	public static void main(String[] args) {
		long T1, T2, T;
		T1 = System.currentTimeMillis();
		fullAdd();
		T2 = System.currentTimeMillis();
		T = T2 - T1;
		System.out.println("\n\t*** Execution time = " + T + " ms");
	}

	private static void fullAdd() {
		Store store = new Store();
		
		IntVar in1 = new IntVar(store, "In1", 0,1);
		IntVar in2 = new IntVar(store, "In2", 0,1);
		IntVar cIn = new IntVar(store, "CarryIn", 0,1);
		IntVar t1 = new IntVar(store, "T1", 0,1);
		IntVar t2 = new IntVar(store, "T2", 0,1);
		IntVar t3 = new IntVar(store, "T3", 0,1);
		IntVar cOut = new IntVar(store, "CarryOut", 0,1);
		IntVar sum = new IntVar(store, "Sum", 0,1);
		
		store.impose(new XorBool(in1,in2,t1));
		store.impose(new AndBool(new IntVar[]{in1,in2}, t2));
		store.impose(new XorBool(t1,cIn,sum));
		store.impose(new AndBool(new IntVar[]{t1,cIn}, t3));
		store.impose(new OrBool(new IntVar[]{t3,t2}, cOut));
		
		
		
		IntVar[] all = {in1,in2,cIn,cOut,sum};
		
		Search<IntVar> label = new DepthFirstSearch<IntVar>();
		
		SelectChoicePoint<IntVar> select = new SimpleSelect<IntVar>(all, null, new IndomainMin<IntVar>());
		label.setSolutionListener(new PrintOutListener<IntVar>());
		label.getSolutionListener().searchAll(true); 
		label.getSolutionListener().recordSolutions(true);
		
		boolean Result = label.labeling(store, select);
		

		
		if(Result) {
			label.getSolutionListener().printAllSolutions();
		} else {
			System.out.println("\n*** No");
		}
		
		
	}

}
